k:Knd, T, B:Type, l:IdLnk, ds:x:Id fp Type, tg:Id, f:(State(ds)TB), es:ES.
usends1-p(es;ds;k;T;l;tg;B;f)  Prop 

latex

Definitions	t  T, x:A. B(x), source(l), Id, loc(e), E, P  Q, e@i. P(e), valtype(e), P & Q, val(e), Top, IdDeq, x. t(x), f(x)?z, vartype(i;x), State(ds), state@i, (state when e), Knd, IdLnk, a:A fp B(a), ES, 1of(t), A & B, {T}, sender(e), kind(e), rcv(l,tg), Prop, x:A. B(x), usends1-p(es;ds;k;T;l;tg;B;f)
Lemmas	event system wf, decl-state wf, fpf wf, IdLnk wf, subtype rel wf, es-valtype wf, alle-at wf, rcv wf, Knd wf, es-kind wf, es-sender wf, es-kind-rcv, es-state-when wf, subtype rel dep function, subtype rel self, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-val wf, es-E wf, Id wf, es-loc wf, lsrc wf